Inference at * 1 1 
Iof proof for Lemma bool sq:



1. x : ?Unit
2. y : ?Unit
3. x = y
4. case x of inl(x) => x | inr(x) => x = case y of inl(x) => x | inr(x) => x
5. case x of inl(x) => True | inr(x) => False = case y of inl(x) => True | inr(x) => False
  x ~ y 

latex

 by Assert (True = False) 

latex

 1: .....assertion..... NILNIL

 1:   (True = False)
 2: 

 2: 6. (True = False)
 2:   x ~ y
 .

Definitions

A, s = t, , True, False